\begin{tabbing}
$\forall$\=$E$:Type, $T$,$V$:(Id$\rightarrow$Id$\rightarrow$Type), $M$:(IdLnk$\rightarrow$Id$\rightarrow$Type), ${\it pred?}$:($E$$\rightarrow$(?$E$)),\+
\\[0ex]${\it info}$:($E$$\rightarrow$((:Id $\times$ Id) + (:(:IdLnk $\times$ $E$) $\times$ Id))), ${\it init}$:($i$:Id$\rightarrow$EState(($T$($i$)))),
\\[0ex]${\it Trans}$:(\=$i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.($V$($i$,$a$)); $l$,$t$.($M$($l$,$t$)))$\rightarrow$EState(($T$($i$)))$\rightarrow$EState\+
\\[0ex](($T$($i$)))),
\-\\[0ex]${\it val}$:($e$:$E$$\rightarrow$kindcase(kind($e$); $a$.($V$(loc($e$),$a$)); $l$,$t$.($M$($l$,$t$)))), ${\it time}$:($E$$\rightarrow$rationals).
\-\\[0ex]($\forall$$e$:$E$. ($\neg$($\uparrow$first($e$))) $\Rightarrow$ (loc(pred($e$)) = loc($e$) $\in$ Id))
\\[0ex]$\Rightarrow$ SWellFounded(pred!($e$;${\it e'}$))
\\[0ex]$\Rightarrow$ ($\forall$$e$:$E$. state\_when($e$) $\in$ EState(($T$(loc($e$)))))
\end{tabbing}